Nuprl Lemma : cr-effective_wf 13,45

es:ES, SysOut:AbsInterface(Top), f:sys-antecedent(es;Sys), e:E(Sys).
(E(Outr E(Sys))  (effective(e 
latex


Upabstract chain replication
Definitions of Statementeffective(e)
Definitionss = t, t  T, x:AB(x), x:AB(x), ES, EState(T), a:A fp B(a), f(a), Id, , strong-subtype(A;B), P  Q, Type, EqDecider(T), Unit, left + right, IdLnk, x:A  B(x), EOrderAxioms(Epred?info), kindcase(ka.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), type List, , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, e < e', , b, constant_function(f;A;B), SWellFounded(R(x;y)), , pred!(e;e'), x,yt(x;y), !Void(), x:A.B(x), Top, S  T, suptype(ST), first(e), A, <ab>, pred(e), x.A(x), xt(x), P & Q, E, AbsInterface(A), sys-antecedent(es;Sys), E(X), e c e', {x:AB(x)} , e  X, y is f*(x), let x,y = A in B(x;y), t.1, x:AB(x), hd(l), y=f*(x) via L, e loc e' , (e <loc e'), A c B, (x  l), effective(e)
Lemmases-interface wf, fun-path wf, fun-connected wf, es-locl wf, es-le wf, es-is-interface wf, es-causle wf, es-E-interface wf, sys-antecedent wf, es-E wf, deq wf, EOrderAxioms wf, kind wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, not wf, assert wf, first wf, top wf, unit wf, pred! wf, strongwellfounded wf, member wf, rationals wf, Id wf, EState wf, subtype rel wf, event system wf

origin